Termination w.r.t. Q proof of TRS/Cimequick.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> TEST₂(a_4, x)
MATCH_4₂(l_5, Cons₂(a, l')) -> PART₂(a, l')
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> APPEND₂(quick₁(l1), Cons₂(a, quick₁(l2)))
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> MATCH_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> MATCH_2₅(x, l', a_4, l_3, part₂(a_4, l'))
PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> TEST₂(a_4, x)
MATCH_4₂(l_5, Cons₂(a, l')) -> PART₂(a, l')
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> APPEND₂(quick₁(l1), Cons₂(a, quick₁(l2)))
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
MATCH_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> MATCH_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> MATCH_2₅(x, l', a_4, l_3, part₂(a_4, l'))
PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)
MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

PART₂(a_4, l_3) -> MATCH_1₃(a_4, l_3, l_3)

The remaining pairs can at least be oriented weakly.

MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( PART₂(x₁, x₂) ) = x₂ + 1

POL( MATCH_1₃(x₁, ..., x₃) ) = max{0, x₃ - 2}

POL( Cons₂(x₁, x₂) ) = x₂ + 3

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_1₃(a_4, l_3, Cons₂(x, l')) -> PART₂(a_4, l')

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)
APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MATCH_0₃(l1_2, l2_1, Cons₂(x, l)) -> APPEND₂(l, l2_1)

The remaining pairs can at least be oriented weakly.

APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( MATCH_0₃(x₁, ..., x₃) ) = max{0, x₃ - 2}

POL( Cons₂(x₁, x₂) ) = x₂ + 3

POL( APPEND₂(x₁, x₂) ) = max{0, x₁ - 2}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND₂(l1_2, l2_1) -> MATCH_0₃(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_4₂(l_5, Cons₂(a, l')) -> MATCH_5₄(a, l', l_5, part₂(a, l'))
QUICK₁(l_5) -> MATCH_4₂(l_5, l_5)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l2)
MATCH_5₄(a, l', l_5, Pair₂(l1, l2)) -> QUICK₁(l1)

The TRS R consists of the following rules:

test₂(x_0, y) -> True
test₂(x_0, y) -> False
append₂(l1_2, l2_1) -> match_0₃(l1_2, l2_1, l1_2)
match_0₃(l1_2, l2_1, Nil) -> l2_1
match_0₃(l1_2, l2_1, Cons₂(x, l)) -> Cons₂(x, append₂(l, l2_1))
part₂(a_4, l_3) -> match_1₃(a_4, l_3, l_3)
match_1₃(a_4, l_3, Nil) -> Pair₂(Nil, Nil)
match_1₃(a_4, l_3, Cons₂(x, l')) -> match_2₅(x, l', a_4, l_3, part₂(a_4, l'))
match_2₅(x, l', a_4, l_3, Pair₂(l1, l2)) -> match_3₇(l1, l2, x, l', a_4, l_3, test₂(a_4, x))
match_3₇(l1, l2, x, l', a_4, l_3, False) -> Pair₂(Cons₂(x, l1), l2)
match_3₇(l1, l2, x, l', a_4, l_3, True) -> Pair₂(l1, Cons₂(x, l2))
quick₁(l_5) -> match_4₂(l_5, l_5)
match_4₂(l_5, Nil) -> Nil
match_4₂(l_5, Cons₂(a, l')) -> match_5₄(a, l', l_5, part₂(a, l'))
match_5₄(a, l', l_5, Pair₂(l1, l2)) -> append₂(quick₁(l1), Cons₂(a, quick₁(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.